<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | RunningPRISM / ModelChecking 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

.sourceblocklink {
  text-align: right;
  font-size: smaller;
}
.sourceblocktext {
  padding: 0.5em;
  border: 1px solid #808080;
  color: #000000;
  background-color: #f1f0ed;
}
.sourceblocktext div {
  font-family: monospace;
  font-size: small;
  line-height: 1;
  height: 1%;
}
.sourceblocktext div.head,
.sourceblocktext div.foot {
  font: italic medium serif;
  padding: 0.5em;
}

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='StartingPRISM.html'>Running PRISM</a> /
</p><h1>Model Checking</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<p>Typically, once a model has been constructed, it is analysed through model checking.
Properties are specified as described in the "<a class='wikilink' href='../PropertySpecification/Introduction.html'>Property Specification</a>" section,
and are usually kept in files with extensions <code>.props</code>, <code>.pctl</code> or <code>.csl</code>.
There are properties files accompanying most of the sample PRISM models in the <code>examples</code> directory.
</p>
<p class='vspace'><a name='gui' id='gui'></a>
</p><h3>GUI</h3>
<p>To load a file containing properties into the GUI, select menu option "Properties | Open properties list".
The file can only be loaded if there are no errors, otherwise an error is displayed.
Note that it may be necessary to have loaded the corresponding model first,
since the properties will probably make reference to variables (and perhaps constants) declared in the model file.
Once loaded, the properties contained in the file are displayed in a list in the "Properties" tab of the GUI.
Constants and labels are displayed in separate lists below.
You can modify or create new properties, constants and labels from the GUI,
by right-clicking on the appropriate list and selecting from the pop-up menu which appears. Properties with errors are shaded red and marked with a warning sign.
Positioning the mouse pointer over the property displays the corresponding error message.
</p>
<p class='vspace'>The pop-up menu for the properties list also contains a "Verify" option,
which allows you instruct PRISM to model check the currently selected properties
(hold down Ctrl/Cmd to select more than one property simultaneously).
All properties can be model checked at once by selecting "Verify all".
PRISM verifies each property individually.
Upon completion, the icon next to the property changes according to the result of model checking. For Boolean-valued properties, a result of true or false is indicated by a green tick or red cross, respectively. For properties which have a numerical result (e.g. <code>P=? [ ...]</code>), position the mouse pointer over the property to view the result.
In addition, this and further information about model checking is displayed in the log in the "Log" tab.
</p>
<p class='vspace'><a name='cl' id='cl'></a>
</p><h3>Command-line</h3>
<p>From the command-line, model checking is achieved by passing both a model file and a properties file as arguments, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm poll.csl</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='ModelChecking@action=sourceblock&amp;num=1' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>The results of model checking are sent to the display and are as described above for the GUI version.
By default, all properties in the file are checked.
To model check only a single property, use the <code>-prop</code> switch.
For example, to check only the fourth property in the file:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm poll.csl -prop 4</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='ModelChecking@action=sourceblock&amp;num=2' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>or to check only the property with <a class='wikilink' href='../PropertySpecification/PropertiesFiles.html#names'>name</a> "safe" in the file:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm poll.csl -prop safe</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='ModelChecking@action=sourceblock&amp;num=3' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Alternatively, the contents of a properties file can be specified directly from the command-line, using the <code>-pf</code> switch:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm -pf 'P&gt;=0.5 [ true U&lt;=5 (s=1 &amp; a=0) ]'</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='ModelChecking@action=sourceblock&amp;num=4' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>The switches <code>-pctl</code> and <code>-csl</code> are aliases for <code>-pf</code>.
</p>
<p class='vspace'>Note the use of single quotes (<code>'...'</code>) to avoid characters such as
<code>(</code> and <code>&gt;</code> being interpreted by the command-line shell.
Single quotes are preferable to double quotes since PRISM properties often include double quotes, e.g. for references to labels or properties.
</p>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Welcome.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='StartingPRISM.html'>Running PRISM</a></strong>
</p><ul><li><a class='wikilink' href='StartingPRISM.html'>Starting PRISM</a>
</li><li><a class='wikilink' href='LoadingAndBuildingAModel.html'>Loading And Building a Model</a>
</li><li><a class='wikilink' href='DebuggingModelsWithTheSimulator.html'>Debugging Models With The Simulator</a>
</li><li><a class='wikilink' href='ExportingTheModel.html'>Exporting The Model</a>
</li><li><a class='selflink' href='ModelChecking.html'>Model Checking</a>
</li><li><a class='wikilink' href='ApproximateModelChecking.html'>Approximate Model Checking</a>
</li><li><a class='wikilink' href='ComputingSteady-stateAndTransientProbabilities.html'>Computing Steady-state And Transient Probabilities</a>
</li><li><a class='wikilink' href='Experiments.html'>Experiments</a>
</li><li><a class='wikilink' href='Adversaries.html'>Adversaries</a>
</li><li><a class='wikilink' href='SupportForPEPAModels.html'>Support For PEPA Models</a>
</li><li><a class='wikilink' href='SupportForSBML.html'>Support For SBML</a>
</li><li><a class='wikilink' href='ExplicitModelImport.html'>Explicit Model Import</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
